Section: New Results

Information Flow

The analysis of the flow of information in a program consists in detecting the propagation of sensitive information through the program points of this program thanks to a dependency analysis.

Dependency Analysis and Numerical Invariants

Participants : Agostino Cortesi [Università Ca'Foscardi di Venizia] , Matteo Zanioli.

A new framework has been proposed in [16] , that combines variable dependency analysis, based on propositional formulas, and variables' value analysis, based on generic numerical domains.

Leakage Analysis

Participants : Matteo Zanioli [Correspondent] , Pietro Ferrara [ETH, Zurich] , Agostino Cortesi [Università Ca' Foscari] .

In [24] , we present Sails , a new tool that combines Sample , a generic static analyzer, and a sophisticated domain for leakage analysis. This tool does not require to modify the original language, since it works with mainstream languages like Java ™, and it does not require any manual annotation. Sails can combine the information leakage analysis with different heap abstractions, inferring information leakage over programs with complex data structures. Sails has been applied to the analysis of the SecuriBench-micro suite. The experimental results underline the effectiveness of the analysis, since Sails is in position to analyze several benchmarks in about 1 second without producing false alarms in more than 90% of the programs.